A:MsgA.  || A 

latex

Definitions	Knd, t  T, IdLnk, Id, x:A. B(x), x. t(x), a:A fp B(a), product-deq(A;B;a;b), Top, 2of(t), rcv(l,tg), f(x)?z, 1of(t), State(ds), IdLnkDeq, Prop, locl(a), KindDeq, IdDeq, P & Q, Valtype(da;k), mk-ma, MsgA, M1 ||decl M2, M1 || M2,
Lemmas	msga wf, fpf-empty-compatible-left, id-deq wf, Id wf, Kind-deq wf, Knd wf, locl wf, IdLnk wf, idlnk-deq wf, ma-state wf, pi1 wf, top wf, fpf-cap wf, rcv wf, pi2 wf, product-deq wf, fpf-trivial-subtype-top